Nuprl Lemma : ma-prob-da_wf
11,40
postcript
pdf
M
:MsgA. ma-prob-da(
M
)
latex
Definitions
,
Type
,
t
T
,
x
:
A
.
B
(
x
)
,
State(
ds
)
,
x
:
A
B
(
x
)
,
Id
,
x
.
A
(
x
)
,
x
.
t
(
x
)
,
a
:
A
fp
B
(
a
)
,
Top
,
b
,
,
Outcome
,
Knd
,
locl(
a
)
,
f
(
x
)?
z
,
P
Q
,
x
dom(
f
)
,
x
:
A
B
(
x
)
,
P
&
Q
,
b
dom(
M
.prob)
,
a
in dom(
M
.pre)
,
M
.da(
a
)
,
ma-prob(
M
;
b
)
,
ma-prob-da-dom(
M
;
b
)
,
ma-prob-da(
M
)
,
MsgA
Lemmas
fpf-dom
wf
,
assert
wf
,
fpf-trivial-subtype-top
,
ma-state
wf
,
bool
wf
origin
M:MsgA. ma-prob-da(M) 
M:MsgA. ma-prob-da(M) 
Tx:A. B(x)
B(x)
x.A(x)
x. t(x) B(a)
b
Q dom(f)
B(x) dom(M.prob)